es:ES, P:(E).
(e:E. Dec(P(e)))
 (X:AbsInterface(E)
 ((e:E.
 ((((e  X))  (a:E. (es-p-local-pred(es;P)(e,a))))
 (& (((e  X))  (es-p-local-pred(es;P)(e,X(e)))))) 

latex

Definitions	E, x,y. t(x;y), f(a), es-p-local-pred(es;P), P & Q, P  Q, b, AbsInterface(A), strong-subtype(A;B), x.A(x), s = t, ES, x:A. B(x), x:A  B(x), P  Q, x:A. B(x), , Type, x:AB(x), Dec(P), t  T
Lemmas	es-E wf, decidable exists-es-p-local-pred, decidable wf, es-p-local-pred wf, es-interface-from-decidable, event system wf, es-interface wf, iff wf, assert wf